\documentclass{llncs}

\usepackage[linesnumbered]{algorithm2e}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{tikz}
\usepackage{bussproofs}
\usepackage{ stmaryrd }

\newcommand{\hide}[1]{}
\newcommand{\transto}[1]{\overset{#1}{\longrightarrow}}
\newcommand{\pre}[0]{\mathit{Pre}^*}
\newcommand{\FF}{\mathsf{false}}
\newcommand{\TT}{\mathsf{true}}
\newcommand{\bbfB}{\mathbb{B}}
\newcommand{\bbfN}{\mathbb{N}}
\newcommand{\ox}{\overline{X}}
\newcommand{\os}{\overline{S}}
\newcommand{\op}{\overline{P}}
\newcommand{\ot}{\overline{T}}
\newcommand{\PP}{N}

\newcommand{\pss}{\overline{S_s}}
\newcommand{\pst}{\overline{S_t}}
\newcommand{\pds}{\overline{D_s}}
\newcommand{\pdt}{\overline{D_t}}


\newcommand{\ou}{\overline{U}}
\newcommand{\ov}{\overline{V}}
\newcommand{\ow}{\overline{W}}
\newcommand{\TODO}[1]{\textbf{TODO:}{#1}}
\newcommand{\history}[1]{$\mathit{History}^{#1}(x_{s_1}, x_{a_1}, x_{t_1}, \dots, x_{s_{#1}},x_{a_{#1}},x_{t_{#1}})$}
\newcommand{\loopfree}[1]{$\mathit{Loop\textmd{-}free}^{#1}(x_{s_1}, x_{a_1}, x_{t_1}, \dots, x_{s_{#1}},x_{a_{#1}},x_{t_{#1}})$}
\newcommand{\historyOne}[0]{$\mathit{History}^1(x_{s_1}, x_{a_1}, x_{t_1})\ $}
\newcommand{\historyZero}[0]{$\mathit{History}^0()\ $}
\newcommand{\reach}[0]{\mathit{Reach}}
\newcommand{\valueof}[1]{[\![{#1}]\!]}

\usetikzlibrary{arrows}
\usetikzlibrary{shapes}
\usetikzlibrary{automata}

\title{Property Directed Reachability for Pushdown Systems}
\author{Yu-Fang Chen \and Kai-Fu Tang \and Bow-Yaw Wang}

\institute{Academia Sinica, Taiwan}

\pagestyle{plain}
\sloppy

\begin{document}
\maketitle

\begin{abstract}%0.3
We propose a complete SAT-based model checking algorithm for pushdown
systems. Inspired by property directed reachability, our algorithm
computes over-approximations of reachable paths in pushdown
systems. We introduce inductive path invariants to formalize over-approximations
of reachable paths. Our algorithm proves
safety properties of pushdown systems by computing inductive path invariants. If no
such inductive path invariant can be found, our complete algorithm
stops and reports an error.
Experimental results suggest
that our algorithm is significantly more scalable than former symbolic
algorithms. 
\end{abstract}



\section{Introduction} %1p

Recursion is a common programming technique. Verification of recursive programs is thus an important issue. Pushdown systems are natural models for recursive programs in verification. Their configuration reachability problem is known to be decidable~\cite{FinkelWW97}. Efficient algorithms~\cite{FinkelWW97,EsparzaHRS00,rhs:popl:1995} and their implementations~\cite{BallR00,EsparzaS01} are also available. The current implementations use binary decision diagrams (BDD's) to perform symbolic computation.
% drawbacks of BDD-based approaches
Thanks to recent progresses in satisfiability (SAT) solvers, SAT-based techniques have been widely used in verifying finite state systems~\cite{SheeranSS00,McMillan03,Bradley11,pdr,ic3-2}. Compared to BDD-based algorithms, SAT-based techniques are less sensitive to the number of Boolean variables and thus can be more scalable. Their applications however are somewhat limited since arbitrary Boolean quantifications are allowed. Since quantifications are needed in BDD-based verification algorithms for recursive programs, developing complete SAT-based techniques for such programs is challenging.

We present the first complete SAT-based model checking algorithm for
pushdown systems. Our algorithm is a symbolic version of the RHS
algorithm for signature reachability~\cite{rhs:popl:1995}. 
The RHS algorithm can be viewed as a reduction from the pushdown
system model checking problem to the reachability problem of a finite
state system with special transitions
(called \emph{summary rules} in Section~\ref{rhs}). 
Inspired by the property directed reachability (PDR)
algorithm for finite state
systems~\cite{Bradley11,ic3-2,pdr},
we develop a compete SAT-based algorithm for the finite state
reachability problem reduced from the configuration reachability problem for pushdown system through the RHS algorithm.

We introduce inductive path invariants to formalize over-approximations of reachable paths. Similar to PDR, our SAT-based algorithm for pushdown systems computes over-approximations of reachable paths incrementally. It maintains a sequence of over-approximations and refines them by need. The algorithm aims to compute an inductive path invariant stronger than the given safety property.
If such inductive path invariants exist, our algorithm guarantees to find one. 
Otherwise, our algorithm will stop and report an error.
\hide{
a counterexample to the safety property. 
}

%talk about the proof obligations?

We implement our algorithm and compare with the \hide{mature} BDD-based model checker \textsc{Moped2} for pushdown systems.
In addition to the original benchmarks shipped
with \textsc{Moped2}, we enlarge the
variable size in the benchmarks to 8, 16, 32, and 64 bits to
evaluate the scalability of our algorithm. 
Experimental results suggest that our SAT-based algorithm is significantly more scalable than the BDD-based
algorithm. When the variable sizes are increased to 32 and 64 bits,
\textsc{Moped2} runs out of memory and cannot finish any of the
verification tasks in benchmarks. In contrast, our implementation
still finishes more than a half of such verification tasks within the
resource constraints. 

We briefly compare related works in two categories: model checking algorithms for pushdown systems, and SAT-based algorithms for finite state systems.
Two types of model checking algorithms have been proposed for pushdown systems. The configuration-based algorithms~\cite{FinkelWW97,EsparzaHRS00,AlurEY01} compute reachable configurations. The path-based algorithm~\cite{rhs:popl:1995} computes reachable paths (pairs of signatures). Ours is a symbolic version of the path-based algorithm in~\cite{rhs:popl:1995}. 
\hide{
The information stored in configuration-based algorithms is more compact. It would be interesting to develop SAT-based techniques for configuration-based algorithms.
}

Several model checkers for recursive programs are available. Bebop~\cite{BallR00} implements the path-based algorithm and \textsc{Moped}~\cite{EsparzaS01} implements a configuration-based algorithm. Both use BDD's as their symbolic representations. QBF-based techniques have also been proposed for model checking pushdown systems~\cite{CookKS05,BaslerKW07_SPIN,BaslerKW07_HVC}. Since solving QBF is still more expensive in practice, our SAT-based technique is more practical. A complete SAT-based algorithm for context-free processes is proposed in~\cite{HW:10:CSBMCCFP}. Context-free processes is a proper subclass of pushdown systems. To the best of our knowledge, ours is the first complete SAT-based verification algorithm for the general class of pushdown systems.

The first complete SAT-based model checking algorithm is published in ~\cite{SheeranSS00}. It makes use of induction for early termination and loop-free traces for completeness. The complete interpolation-based algorithm is proposed in~\cite{McMillan03}. The PDR algorithm is develop in~\cite{Bradley11}. Our algorithm is a generalization of the PDR algorithm to pushdown systems. In order to support summary rules, we generalize proof obligations to record \emph{sets} of paths. We are unaware of such generalizations.
\hide{
Our first attempt of SAT-based pushdown model checking algorithm uses the idea of~\cite{SheeranSS00}. However, this version performs badly in the \textsc{Moped2} benchmarks. The current version is inspired by the property directed reachability (PDR) algorithm~\cite{pdr}.
}

The organization is as follows. Pushdown systems are defined in Section~\ref{pds}. Section~\ref{rhs} reviews the path-based algorithm for pushdown systems in~\cite{rhs:popl:1995}. It is followed by our technical contribution (Section~\ref{pds-pdr}). We report experimental results in Section~\ref{exps}. Finally, Section~\ref{conclusions} concludes our presentation.

\section{Pushdown System}
\label{pds}
A \emph{pushdown system (PDS)} is a tuple $P = ( Q, \Gamma, q_0, \gamma_0,
\Delta )$ where $Q$ is a finite set of \emph{states},
$\Gamma$ a finite set of \emph{stack symbols}, $q_0 \in Q$ an
\emph{initial state}, $\gamma_0 \in \Gamma$ an
\emph{initial stack symbol}, and $\Delta \subseteq Q \times \Gamma \times Q \times
\Gamma^{\leq 2}$ a \emph{transition relation}. We write $(p, a)
\hookrightarrow (q, w)$ when $(p, a, q, w) \in \Delta$. Note that this formulation of transition relation is sufficient to describe typical pushdown operations such as~\emph{push}~and~\emph{pop}.

Given a PDS $P = ( Q, \Gamma,
q_0, \gamma_0, \Delta )$, 
a \emph{configuration}  of $P$ is a pair $(q, \gamma)$, where $q \in Q$
is a state and $\gamma \in \Gamma^*$ is the stack content.
For any configuration $(p, a\gamma )$, $(q, w\gamma )$ is a
\emph{successor} of $(p, a\gamma )$ in $P$ if $(p, a) \hookrightarrow
(q, w)$. We say that a configuration $(p_n, \gamma_n)$ is
\emph{reachable} from a configuration $(p_1, \gamma_1)$ if there
exists a sequence of configurations $(p_1, \gamma_1)(p_2,
\gamma_2)\ldots (p_n, \gamma_n)$ such that $(p_{i+1}, \gamma_{i+1})$
is a successor of $(p_i, \gamma_i)$ in $P$ for $ 0 < i < n$. We say
that a configuration is reachable in $P$ if it is reachable from the
initial configuration $(q_0, \gamma_0)$.

\subsubsection*{Signature Reachability}
Let $P = ( Q, \Gamma, q_0, \delta_0, \Delta )$ be a
pushdown system. A \emph{signature} $(p, a) \in Q \times \Gamma$
consists of a state $p$ and a stack symbol $a$. The signature $(p, a)$
is \emph{reachable} if the configuration $(p, a\gamma)$ is reachable
for some $\gamma \in \Gamma^*$. Consider a set $\mathit{Sig} \subseteq
Q \times \Gamma$ of \emph{target} signatures. The \emph{signature reachability
problem} for the pushdown system $P$ is to check if there is a reachable signature in $\mathit{Sig}$.
\hide{
For short, we also call it a PDS reachability problem.
}
In this paper, we propose a SAT-based algorithm to solve the signature
reachability problem for pushdown systems.

\section{The RHS Algorithm for Signature Reachability}
\label{rhs}
%Let $\bbfB = \{ \FF, \TT \}$ be the \emph{Boolean domain} with
%\emph{truth values} $\FF$ and $\TT$. For any finite set $\ox$ of
%Boolean variables, define $\ox' = \{ x' : x \in \ox \}$, $\ox_0 = \{
%x_0 : x \in \ox \}$, and $\ox_1 = \{ x_1 : x \in \ox \}$.
%A \emph{valuation} of $\ox$ is a mapping from $\ox$ to $\bbfB$. If $v$
%is a valuation of $\ox$, define the valuations $v' (x') = v_0 (x_0) =
%v_1 (x_1) = v (x)$ for every $x \in \ox$. Observe that $v'$, $v_0$,
%and $v_1$ are valuations of $\ox'$, $\ox_0$, and $\ox_1$ respectively.
%For any Boolean formula $F$ over $\ox$, $F'$, $F^0$, $F^1$ denote the
%Boolean formulae obtained by substituting $\ox'$, $\ox_0$, $\ox_1$ for
%$\ox$ in $F$ respectively.



%We also fix $\os$ and $\ot$ to be finite sets of Boolean \emph{state} and
%\emph{stack} variables respectively. A \emph{state} in $Q$ is a valuation of
%$\os$; a \emph{stack symbol} in $\Gamma$ is a valuation of $\ot$. A
%\emph{configuration} $(p, a)$ is a pair of state $p$ and a stack symbol $a$.

%Define three PDS transition functions $\chi_{\Delta_0}$ over $\os,\ot,\os_1$ (pop operation), $\chi_{\Delta_1}$  over $\os,\ot,\os_1,\ot_1$ (intra-procedure operation), $\chi_{\Delta_2}$ over $\os,\ot,\os_1,\ot_1,\ot_2$ (push operation) as follows.
%\begin{enumerate}
%\item $\chi_{\Delta_0}(p, a, q_1)=\TT$ iff $(p,a, q) \in \Delta$\\
%\item $\chi_{\Delta_1}(p, a, q_1, a_1)=\TT$ iff $(p,a, q, a_1) \in \Delta$\\
%\item $\chi_{\Delta_2}(p, a, q_1, a_1, a_2)=\TT$ iff $(p,a, q, a_1, a_2) \in \Delta$\\
%\end{enumerate}

The RHS algorithm solves the signature reachability problem for pushdown systems~\cite{rhs:popl:1995}. Let us call a pair of signatures by a \emph{path}. The first signature of a path records the \emph{input} signature at the entry of a function call; the second is a signature reachable from the first. 
The RHS algorithm has three transition rules. 
Starting from the \emph{initial path} $((q_0,\gamma_0),(q_0,\gamma_0))$, each rule derives a path by existing paths and transitions in the pushdown system. 
A path is \emph{reachable} if it can be derived from the initial path using the three transition rules. In order to compute reachable paths, 
the RHS algorithm maintains a set $E$ of paths. Initially, the set $E$ contains only the initial path. The algorithm adds more paths to the set $E$ by applying its transition rules repeatedly. It can be shown that a signature $(s,x)$ is reachable iff there is a reachable path $((q,w),(s,x))$ for some signature $(q,w)$.
We use $(q,w)\hookrightarrow_E(s,x)$ to denote that the path $((q,w),(s,x))\in E$.
\\
\textbf{Intra-procedure rule:}
\begin{prooftree}
\AxiomC{$(p, r) \hookrightarrow_E  (q, w)$}
\AxiomC{$(q, w) \hookrightarrow  (s, x)$}
\BinaryInfC{$(p, r) \hookrightarrow_E  (s,x)$}
\end{prooftree}
The first rule describes the situation when an intra-procedure operation is performed. If we know that from the signature $(p,r)$ one can reach the signature $(q,w)$ and $(q, w) \hookrightarrow  (s, x)$ is a transition in the PDS. That is, there is an intra-procedure operation from $(q,w)$ to $(s,x)$. Then the signature $(s,x)$ can also be reached from $(p,r)$. Therefore, we derive~$(p, r) \hookrightarrow_E  (s,x)$.\\\ \\
\textbf{Push rule:}
\begin{prooftree}
\AxiomC{$(p, r) \hookrightarrow_E  (q, w)$}
\AxiomC{$(q, w) \hookrightarrow  (s, xz)$}
\BinaryInfC{$(s, x) \hookrightarrow_E  (s,x)$}
\end{prooftree}

The second rule describes the situation when a a function call is performed. If we know that from the signature $(p,r)$ one can reach the signature $(q,w)$ and $(q, w) \hookrightarrow  (s, xz)$  is a transition in the PDS. That is, there is a push operation for a function call with the input signature $(s,x)$. Then we can add the path $((s,x),(s,x))$ to $E$. The first element of the path means that $(s,x)$ is a reachable signature and the second element says that $(s,x)$ is reachable from itself.\\\ \\
\textbf{Summary rule:}
\begin{prooftree}
\AxiomC{$(p, r) \hookrightarrow_E  (q, w)$}
\AxiomC{$(q, w) \hookrightarrow (u, ax)$}
\AxiomC{$(u, a) \hookrightarrow_E  (v, b) \ \ \ \ (v, b) \hookrightarrow (s, \lambda)$}
\TrinaryInfC{$(p, r) \hookrightarrow_E  (s, x)$}
\end{prooftree}

The third rule describes the case when a \emph{summary edge} is used. A summary edge records an input and output signature pair of a function call. In the rule above, from the two PDS transitions $(q, w) \hookrightarrow (u, ax)$ (push), $(v, b) \hookrightarrow (s, \lambda)$ (pop), and the fact that $(u, a) \hookrightarrow_E  (v, b)$, one derives that if $(q,w)$ can be reached from $(p, r)$, then $(s, x)$ can also be reached from $(p,r)$.


\subsection*{Symbolic Encoding}


Let $\bbfB = \{ \FF, \TT \}$ be the \emph{Boolean domain} with
\emph{truth values} $\FF$ and $\TT$. For any finite set $\ox$ of 
Boolean variables, define $\ox' = \{ x' : x \in \ox \}$ and $\ox^n = \{
x^n : x \in \ox \}$ for all $n\in \mathbb{N}$.
A \emph{valuation} of $\ox$ is a mapping from $\ox$ to $\bbfB$. If $v$
is a valuation of $\ox$, define the valuations $v' (x') = v^0 (x^0) =
v^1 (x^1) = v (x)$ for every $x \in \ox$. Observe that $v'$, $v^0$,
and $v^1$ are valuations of $\ox'$, $\ox^0$, and $\ox^1$ respectively.
For any Boolean formula $F$ over $\ox$ and $n\in\mathbb{N}$, $F'$ and $F^n$ denote the
Boolean formulae obtained by substituting $\ox'$ and $\ox^n$ for
$\ox$ in $F$ respectively. 

Fix a finite set $\op$ of Boolean \emph{path} variables. 
Recall that a path is a pair of signatures. A valuation of path variables corresponds to a path in $Q \times \Gamma \times Q \times \Gamma$. For a valuation $\sigma$ of path variables, we also use $\sigma$ to denote its corresponding path by abusing notation.
The intra-procedure and push RHS transition rules can be encoded by the formula $T_1$ over $\op,\op'$. The variables $\op$ denote the path already in the set $E$. The variables $\op'$ denote the path to be added to $E$ by the intra-procedure or push RHS transition rules and the path encoded in $\op$. 
More precisely, $T_1$ is a Boolean formula over $\op, \op'$.
We have $\sigma, \tau' \models T_1$ iff the path $\tau$ can be added to $E$ by the intra-procedure or push rules when $\sigma$ is already in $E$.

Similarly, the summary RHS transition rule can be encoded by the formula $T_2$ over $\op^{0},\op^{1}, \op'$. The variables $\op_0,\op_1$ denote the paths already in the set $E$. The variables $\op'$ denote the path to be added to $E$ by the summary rule and the paths encoded in $\op^0,\op^1$. 
Precisely, $T_2$ is a Boolean formula over $\op^0, \op^1, \op'$.
We have $\sigma^0, \kappa^1, \tau' \models T_2$ iff the path $\tau$ can be added to $E$ by the summary rule when $\sigma$ and $\kappa$ are already in $E$.
Details of the encoding are shown in Appendix~\ref{encoding}.

\section{Algorithms}
\label{pds-pdr}

A \emph{literal} in a Boolean formula is either a Boolean variable or its negation. A \emph{clause} is a disjunction of a set of literals. A clause $c$ is a \emph{subclause} of another clause $d$ if $c \subseteq d$. A \emph{cube} is a conjunction of a set of literals. Similarly, we say that a cube $c$ is a \emph{subcube} of another cube $d$ if $c \subseteq d$. In the sequel, we may alternatively specify a clause or a cube by a set of literals. A Boolean formula is in \emph{conjunction normal form} (CNF) if it is a conjunction of a set of clauses. Similarly, we may alternatively specify a Boolean formula in CNF by a set of clauses. We write $\sigma \models F$ if the Boolean formula $F$ evaluates to $\TT$ under the valuation $\sigma$. We write $\models F$ when $F$ always evaluates to $\TT$. Given a valuation $\sigma$ of path variables $\op$, we use $\langle \sigma \rangle$ to denote the cube $\{x \mid \sigma \models x, x \in \op \}\cup \{\neg x \mid \sigma \models \neg x, x \in \op \}$ and use $\neg \langle \sigma \rangle$ to denote the clause $\{\neg x\mid \sigma \models x, x\in \op \}\cup \{x \mid \sigma \models \neg x, x\in \op \}$. Given a Boolean formula $F$ over Boolean variables $\ox$, we define $\valueof{F}$ as the set of \emph{satisfying valuations} to $F$, that is, $\valueof{F} =\{\sigma \mid \sigma \models F \mbox{ and $\sigma$ is a valuation of $\ox$}\}$.

\subsection{Basic Version}

Let $I$ be a cube that encodes the initial path $((q_0,\gamma_0),(q_0,\gamma_0))$.
An \emph{inductive path invariant} $G$ is a Boolean formula over
$\op$ such that
\begin{enumerate}
\item $\models I \implies G$;
\item $\models G \wedge T_1 \implies G'$; and
\item $\models G^0 \wedge G^1 \wedge T_2 \implies G'$.
\end{enumerate}
For an arbitrary Boolean formula $\PP$ over $\op$, we would like to compute an
inductive path invariant $G$ such that $\models G \implies \PP$. 
For the signature reachability problem, we use $\PP$ to encode all paths not ending in the target signatures $Sig$.

Our approach to find inductive path invariant is described in Algorithm~\ref{algorithm:basic-property-directed-reachability}. We say that a path is in timeframe $n$ if it can be produced by applying the transition formulae $T_1$ and $T_2$ $n$ times. Formally, we use $E_n$ to denote the set of all paths in timeframe $n$.
We have (1) $E_0  =  \{ \sigma : \sigma \models I \}$ and (2) $E_{i+1}  =  
    E_i \cup
    \{ \tau : \sigma, \tau' \models T_1
    \textmd{ with } \sigma \in E_i \} \cup
    \{ \tau : \sigma^0, \kappa^1, \tau' \models T_2
    \textmd{ with } \sigma, \kappa\in E_i \}$.
In Algorithm~\ref{algorithm:basic-property-directed-reachability}, $F_i$ is a CNF formula that encodes an over-approximation of paths in timeframe~$i$. 
The following lemma holds for all $F_i$.
\begin{lemma}
  $\sigma \in E_i$ implies $\sigma \models F_i$ for
  every $0 \leq i \leq k$.
\end{lemma}

\begin{algorithm}
  $k, F_0 \leftarrow 0, I$\;
  \While{$\TT$} 
  {
    \uIf{$\tau \models F_k \wedge \neg \PP$}
    {\label{bpdr3}
      \lIf{$\neg \textup{\textsf{BlockCube}}(k, \langle \tau
        \rangle)$}\label{bpdr4}
      { 
        \Return \texttt{REACHABLE}\; 
      }
    } \uElse {\label{bpdr5}
      $F_{k+1} \leftarrow \TT$\; \label{bpdr6}
      \lIf{$F_i = F_{i+1}$ for some $0 \leq i \leq k$} 
      { \Return \texttt{UNREACHABLE}\; } \label{bpdr7}
      $k \leftarrow k + 1$\; \label{bpdr8}
    }
  }
  \medskip
  \caption{Basic Property Directed Reachability}
  \label{algorithm:basic-property-directed-reachability}
\end{algorithm}

Below we show that when the Algorithm~\ref{algorithm:basic-property-directed-reachability} terminates and reports \texttt{UNREACHABLE}, then there exists some $F_i$ such that $F_i$ is an inductive path invariant.
In order to show this, we first define the condition $\Pi (\PP, F_0, F_1, \ldots, F_k)$.

\begin{definition}
  Let $F_0, F_1, \ldots, F_k$ and $\PP$ be Boolean formulae over $\op$. The condition \emph{$\Pi (\PP, F_0, F_1, \ldots, F_k)$} holds if
  for every $0 \leq i < k$,
  \begin{enumerate}
  \item $F_0 = I$;
  \item $\models F_i \implies F_{i+1}$;
  \item $\models F_i \wedge T_1 \implies F'_{i+1}$;
  \item $\models F^0_i \wedge F^1_i \wedge T_2 \implies F_{i+1}'$; and
  \item $\models F_i \implies \PP$.
  \end{enumerate}
\end{definition}

Initially, Algorithm~\ref{algorithm:basic-property-directed-reachability} sets $F_0 = I$ at iteration $0$. The condition $\Pi (\PP,
F_0)$ holds because there exists no $i$ with $0 \leq i < k$ and hence the requirements $2$ to $5$  of  $\Pi (\PP,
F_0)$ hold vacuously when $k=0$.
Assume the condition $\Pi (\PP, F_0, F_1, \ldots,
F_k)$ holds at the beginning of iteration $k$. Our algorithm
checks if $\models F_k \implies \PP$ (Line~\ref{bpdr3}). If not, it calls 
the function \textup{\textsf{BlockCube}} $(k, \langle \tau \rangle)$
to exclude any path $\tau$ with $\tau \models F_k \wedge \neg
\PP$ from $F_k$ (Line~\ref{bpdr4}).

If the iteration $k$ successfully removes all such
paths, we have $\models F_k \implies \PP$ (Line~\ref{bpdr5}). The algorithm then 
sets $F_{k+1} = \TT$ (Line~\ref{bpdr6}). Note that the condition $\Pi (\PP, F_0, F_1, \ldots,
F_{k+1})$ holds at Line~\ref{bpdr7}. If furthermore $F_i = F_{i+1}$ (notice that $F_i$ and $F_{i+1}$ are sets of clauses) for some $i$, we also have 
$\models F_i \wedge T_1 \implies F'_i$ and $\models F^0_i
\wedge F^1_i \wedge T_2 \implies F'_i$. 
It follows that $F_i$ is in fact an inductive
path invariant. The basic algorithm hence reports
\texttt{UNREACHABLE}. Otherwise it proceeds to iteration $k+1$ (Line~\ref{bpdr8}).
Note that there exists only a finite number of different clauses (recall that a clause is a set of literals) over a finite set of variables. Hence the number of different CNF formulae (set of clauses) is also finite.
Therefore $F_i = F_{i+1}$ will hold eventually and guarantees termination.

\subsection*{The $\mathsf{BlockCube}$ function}
We begin with a high level explanation of the idea behind and then proceed to Algorithm~\ref{algorithm:basic-blockcube} that does the job.
Let $\tau$ be a path with $\tau \models F_k$. Assume that the 
condition $\Pi (\PP, F_0, F_1, \ldots, F_k)$ holds. The function
$\mathsf{BlockCube} (k, \langle \tau \rangle)$ returns $\TT$ if the
path $\tau$ can be removed from $\valueof{F_k}$ while keeping the condition $\Pi (\PP, F_0, F_1, \ldots, F_k)$; otherwise, it returns $\FF$. The function removes the path $\tau$ by adding
clauses to $F_0, F_1, \ldots, F_k$. 

Consider removing a path $\tau$ from $\valueof{F_k}$. Suppose there
is a path $\sigma$ with $\sigma, \tau' \models F_{k-1} \wedge T_1
\wedge \langle \tau' \rangle$. Observe that $\sigma \in
\valueof{F_{k-1}}$ and $\tau \in \valueof{F_k}$. Simply removing
$\tau$ from $\valueof{F_k}$ would 
not maintain the requirement $\models F_{k-1} \wedge T_1 \implies
F'_k$ in the condition $\Pi (\PP, F_0, F_1, \ldots, F_k)$. In order to
fulfill the condition $\Pi (\PP, F_0, F_1, \ldots, F_k)$, one has to
remove the path $\sigma$ from $\valueof{F_{k-1}}$ as well.
Similarly, when there are paths $\sigma$
and $\kappa$ with $\sigma^0, \kappa^1, \tau' \models F^0_{k-1} \wedge
F^1_{k-1} \wedge T_2 \wedge \langle \tau' \rangle$, both
$\sigma$ and $\kappa$ belong to $\valueof{F_{k-1}}$. Removing $\sigma$ \emph{or}
$\kappa$ suffices to maintain the condition $\Pi (\PP, F_0, F_1, \ldots,
F_k)$ if $\tau$ is to be removed from $\valueof{F_k}$. One thus has to remove $\sigma$ or remove $\kappa$ from $\valueof{F_{k-1}}$.

To keep track of paths to be removed, we generalize proof
obligations introduced in~\cite{Bradley11}. Assume the condition $\Pi
(\PP, F_0, 
F_1, \ldots, F_k)$ holds. A \emph{proof obligation $(i, \mathit{Ob})$}
consists of an integer $0 \leq i \leq k$ and a set $\mathit{Ob}$ of
cubes such that  
\begin{enumerate}
\item $\tau \models F_i$ for every $\langle \tau \rangle \in
  \mathit{Ob}$; and
\item $\tau \not\models F_{i-1}$ for some $\langle \tau \rangle \in
  \mathit{Ob}$. 
\end{enumerate}

% intuitions about proof obligations

In order to understand proof obligations, consider the proof obligation
$(i, \{ \langle \tau \rangle \})$. Suppose $\sigma^0, \kappa^1, \tau' \models F^0_{i-1} \wedge F^1_{i-1} \wedge T_2$. Then
$\sigma$ or $\kappa$ must be removed from $\valueof{F_{i-1}}$ before
$\tau$ is removed from $\valueof{F_{i}}$. We hence construct another
proof obligation $(i - 1, \{ \langle \sigma \rangle, \langle \kappa
\rangle \})$. Suppose, furthermore,
$\omega, \sigma' \models F_{i-2} \wedge T_1$ and 
$\epsilon^0, \delta^1,
\kappa' \models F^0_{i-2} \wedge F^1_{i-2} \wedge T_2$. Let us assume
that $\omega$ can be removed from $\valueof{F_{i-2}}$. Then
$\omega, \sigma' \not\models F_{i-2} \wedge T_1$. If there is no other
path $\xi$ such that $\xi, \sigma' \models F_{i-2} \wedge T_1$,
$\sigma$ can be removed from $\valueof{F_{i-1}}$ safely.
Similarly, if $\epsilon$ or $\delta$ is removed from
$\valueof{F_{i-2}}$, $\epsilon^0, \delta^1,
\kappa' \not\models F^0_{i-2} \wedge F^1_{i-2} \wedge T_2$. If there
are no other paths $\xi, \zeta$ such that $\xi^0, \zeta^1, \kappa'
\models F^0_{i-2} \wedge F^1_{i-2} \wedge F_2$, $\kappa$ can be
removed from $\valueof{F_{i-1}}$ safely.
In other words, it suffices to remove any of $\omega, \epsilon, \delta$
from $\valueof{F_{i-2}}$ in order to remove $\sigma$ or $\kappa$ from
$\valueof{F_{i-1}}$. We hence create the proof obligation $(i - 2, \{
\langle \omega \rangle, \langle \epsilon \rangle, \langle \delta
\rangle \})$. Intuitively, the cube set in a proof obligation 
corresponds to a conjunctive requirement. The proof obligation is
valid if all cubes in the set are present. To discharge a proof 
obligation, it suffices to remove one cube from the requirement.

Formally, a cube $\langle \tau \rangle$ is \emph{blocked} at $F_i$
if $\tau 
\not\models F_i$. A set $\mathit{Ob}$ of cubes is \emph{blocked} if a
cube in $\mathit{Ob}$ is blocked. 
A proof obligation $(i, \mathit{Ob})$ is \emph{discharged} by
adding clauses to $F_0, F_1, \ldots, F_i$ so that $\mathit{Ob}$ is
blocked. In order to discharge a proof 
obligation while maintaining the condition $\Pi (\PP, F_0, F_1, \ldots,
F_k)$, more proof obligations may be introduced. We hence maintain a
queue of proof obligations. 

Algorithm~\ref{algorithm:basic-blockcube} describes the details of the function $\mathsf{BlockCube} (k, \langle 
\tau \rangle)$.
It maintains a priority queue $Q$ of proof obligations.
Initially, it adds the proof obligation $(k, \{ \langle \tau \rangle
\})$ to the queue $Q$. 
The algorithm hence tries to remove $\tau$ from $\valueof{F_k}$.




\begin{algorithm}[h]
  \KwIn{$k$ : $\bbfN$; $\langle \tau \rangle$ : $\tau \models F_k$
    where $\Pi (\PP, F_0, F_1, \ldots, F_k)$ holds}
  $Q \leftarrow \textsf{EmptyQueue}$\;
  add $(k, \{ \langle \tau \rangle \})$ to $Q$\;\label{bbc2}
  \While{$Q$ is not empty} {
    pop $(i, \mathit{Ob})$ with the smallest $i$ from $Q$\;\label{bbc4}
    \lIf{$\mathit{Ob}$ is blocked}\label{bbc5}
    { \textbf{continue}\; }
    \lIf{$i = 0$} 
    { 
      \Return $\FF$\; 
    }\label{bbc6}
    $\mathit{Ob}', \mathit{blocked} \leftarrow \varnothing, \FF$\;
    \label{bcc7}
    \ForEach{$\langle \tau \rangle \in \mathit{Ob}$} {\label{bbc8}
      \lIf {$\tau \models I$} 
      { \label{bbc9}
        \textbf{continue}\;
      }
      \uIf {$\sigma, \tau' \models
        \neg \langle \tau \rangle \wedge F_{i-1} \wedge T_1
        \wedge \langle \tau' \rangle$} 
      {\label{bbc11}
        $\mathit{Ob}' \leftarrow \mathit{Ob}' \cup \{ \langle \sigma
        \rangle \}$\;
      } \uElseIf {$\sigma^0, \kappa^1, \tau' \models
        \neg \langle \tau^0 \rangle \wedge
        \neg \langle \tau^1 \rangle \wedge
        F_{i-1}^0 \wedge F_{i-1}^1 \wedge T_2 \wedge
        \langle \tau' \rangle$} 
      {\label{bbc13}
        $\mathit{Ob}' \leftarrow \mathit{Ob}' \cup \{ \langle \sigma
        \rangle, \langle \kappa \rangle \}$\; 
      } \uElse 
      {\label{bbc15}
%        \tcp{$\langle \tau \rangle$ is blocked }
        \lForEach{$1 \le j \le i$} 
        {
          $F_j \leftarrow F_j \cup \{ \neg \langle \tau \rangle \}$\;
        }
        $\mathit{blocked} \leftarrow \TT$\;
        add $(i + 1, \mathit{Ob})$ to $Q$\;
        \textbf{break}\;
      }
    }
    \uIf{$\neg \mathit{blocked}$} {\label{bbc21}
      add $(i, \mathit{Ob})$ and $(i-1, \mathit{Ob}')$ to $Q$\;
    }
  }
  \Return $\TT$\;
  
  \medskip
  \caption{Basic $\textsf{BlockCube}(k, \langle \tau \rangle)$}
  \label{algorithm:basic-blockcube}
\end{algorithm}


In each iteration of the loop, the algorithm picks a proof obligation  $(i, \mathit{Ob})$ with the smallest $i$ from $Q$ (Line~\ref{bbc4}) and tries to discharge it.
Algorithm~\ref{algorithm:basic-blockcube} first checks if
$\mathit{Ob}$ is already blocked (Line~\ref{bbc5}). If the set of cubes is not blocked and $i =
0$, the proof obligation cannot be discharged. The algorithm hence
returns $\FF$ (Line~\ref{bbc6}). If $i > 0$, Algorithm~\ref{algorithm:basic-blockcube}
tries to discharge the proof obligation by blocking $\mathit{Ob}$.
Since another proof obligation $(i - 1, \mathit{Ob}')$ may be
introduced, the algorithm initializes $\mathit{Ob}'$ to be the empty
set (Line~\ref{bcc7}).

To block the set $\mathit{Ob}$,
Algorithm~\ref{algorithm:basic-blockcube} goes through each cube
$\langle \tau \rangle$ in $\mathit{Ob}$ iteratively. We the following
scenarios: 
\begin{enumerate}
\item If $\tau \models I$, the path
$\tau$ cannot be removed from $\valueof{F_i}$ while maintaining the
condition $\Pi (\PP, F_0, F_1, \ldots, F_k)$. The algorithm continues
with another cube in $\mathit{Ob}$ (Line~\ref{bbc9}).
\item If there is a path $\sigma$ with $\sigma, \tau' \models \neg
\langle \tau \rangle \wedge F_{i-1} \wedge T_1 \wedge \langle \tau'
\rangle$ (Line~\ref{bbc11}), the path $\sigma$ has to be removed from
$\valueof{F_{i-1}}$ before $\tau$ is removed from $\valueof{F_i}$. Algorithm~\ref{algorithm:basic-blockcube} thus
adds $\langle \sigma \rangle$ to the
set $\mathit{Ob}'$ of the induced proof obligation. It then continues with
another cube in $\mathit{Ob}$.
\item If there are paths $\sigma$ and $\kappa$ with $\sigma^0,
\kappa^1, \tau' \models \neg \langle \tau^0 \rangle \wedge \neg
\langle \tau^1 \rangle \wedge F^0_{i-1} \wedge F^1_{i-1} \wedge T_2
\wedge \langle \tau' \rangle$ (Line~\ref{bbc13}), $\sigma$ or $\kappa$ must be removed
from $\valueof{F_{i-1}}$ before $\tau$ is removed from $\valueof{F_i}$. Algorithm~\ref{algorithm:basic-blockcube}
adds both $\langle \sigma \rangle$ and $\langle \kappa \rangle$ to
$\mathit{Ob}'$ of the induced proof obligation. It then continues with
another cube in $\mathit{Ob}$.
\item If none of the previous two scenarios occurs (Line~\ref{bbc15}), the path $\tau$ can be
safely removed from $\valueof{F_i}$ by adding the clause $\neg \langle
\tau \rangle$ to $F_1, F_2, \ldots, F_i$. Moreover the set $\mathit{Ob}$ is blocked. The
current proof obligation $(i, \mathit{Ob})$ is discharged. The
algorithm ignores the remaining cubes in the set $\mathit{Ob}$ by
aborting the loop.
\item Finally, if the set $\mathit{Ob}$ cannot be blocked (Line~\ref{bbc21}), the proof
obligation $(i, \mathit{Ob})$ is not
discharged. Algorithm~\ref{algorithm:basic-blockcube} puts the
original proof obligation $(i, \mathit{Ob})$ and the induced proof
obligation $(i - 1, \mathit{Ob}')$ to the queue. It will pop the proof
obligation $(i - 1, \mathit{Ob}')$ and try to block it later.
\end{enumerate}

Algorithm~\ref{algorithm:basic-blockcube} tries to discharge every
proof obligation in the priority queue. When
all proof obligations are discharged, the algorithm returns
$\TT$. Otherwise, a reachable target signature in
$\mathit{Sig}$ is found. The algorithm hence returns $\FF$. The basic
$\mathsf{BlockCube} (k, \langle \tau \rangle)$ function is very
inefficient. It discharges a proof obligation by blocking only one
cube in the cube set. Numerous proof obligations will be
introduced during verification. The basic algorithm cannot be efficient. 
  
  
\subsection{Optimized Version}

\hide{
The optimized version follows the framework of basic version. During the blocking procedure, $\Pi(\PP, F_0, F_1, \dots, F_k)$ holds.
To increase performance, it equips with two features
\textsf{GeneralizeSat} and \textsf{GeneralizeCube}. 

When removing a path $\tau$ from $\valueof{F_k}$, if there is a
path $\tau$ with $\sigma, \tau' \models F_{k-1} \wedge T_1 \wedge
\langle \tau' \rangle$, instead of removing one path $\sigma$ from
$F_{k-1}$, we would like to remove as many paths as possible. 
We therefore find a subcube of the path $\sigma$ so that the
subcube still satisfies $F_{k-1} \wedge T_1 \wedge \langle \tau' \rangle$.
}

The optimized property directed reachability algorithm is almost
identical to the basic version.
At iteration $k$, the optimized algorithm again tries to remove every
path $\tau$ with $\tau \models F_k \wedge \neg P$ from
$\valueof{F_k}$. Instead of just blocking the cube $\langle \tau
\rangle$, the optimized algorithm
computes a cube $\langle \tau_p \rangle \subseteq \langle \tau
\rangle$ such that $ \models \langle \tau_p \rangle \implies F_k \wedge \neg P$, and then blocks
the cube $\langle \tau_p \rangle$ 
(Algorithm~\ref{algorithm:optimized-property-directed-reachability}).

\hide{
To remove a literal from $\langle \tau_r \rangle$, we replace the literal by $\perp$ and perform ternary simulation with the following three rules:
\begin{align*}
0 \wedge \perp = 0\\
1 \wedge \perp = \perp\\
\neg \perp = \perp
\end{align*}
Once the simulation result makes $\Phi = \perp$, the literal cannot be removed. If, on the other hand, the result maintains $\Phi = 1$, we can remove the desired literal.
}

\begin{algorithm}[h]

\hide{
    $k, F_0, C_0 = 0, I, \varnothing$\;
}
    $k, F_0 = 0, I$\;

    \While{$\TT$}
    {
        \uIf{$\tau \models F_k \wedge \neg P$}
        {
            $\langle \tau_p \rangle \leftarrow 
            \textsf{GeneralizeSat}(F_k \wedge \neg P, \langle \tau \rangle)$\;
            \lIf{$\neg \textup{\textsf{BlockCube}}(k, \langle \tau_p \rangle)$} { \Return \texttt{REACHABLE}\; }
        }
        \uElse {
%            $F_k(p,r,q,w) \leftarrow F_k(p,r,q,w) \wedge \neg P(w)$\;
            $k \leftarrow k + 1$\;
            $F_k \leftarrow \TT$\;
\hide{
            $C_k \leftarrow \varnothing$\;
}

            \lIf{$\textup{\textsf{Propagate}}(F_1, F_2, \ldots, F_k)$}
            { \Return \texttt{UNREACHABLE}\; } 
            \label{opdr-propagate}
        }
    }
  \medskip
  \caption{Optimized Property Directed Reachability}
  \label{algorithm:optimized-property-directed-reachability}
\end{algorithm}

Let $\Phi$ be a Boolean formula over $\ox$, and $\tau$ a valuation of
$\ox$ with $\models \langle \tau \rangle \implies \Phi$.
The function $\textsf{GeneralizeSat}(\Phi, \langle \tau \rangle)$
returns a cube $\langle \sigma \rangle \subseteq \langle \tau \rangle$
such that $\models \langle \sigma \rangle \implies \Phi$. In other
words, $\langle \sigma \rangle$ contains necessary literals of
$\langle \tau \rangle$ to satisfy $\Phi$. The function
$\mathsf{GeneralizeSat} (\Phi, \langle \tau \rangle)$ can be
implemented, for example, by extracting from satisfying
assignments in SAT solvers. Our implementation uses ternary
simulation~\cite{pdr}. The following observation will be useful to 
our exposition: 

\begin{proposition}
  Let $\Phi$ be a Boolean formula over $\ox$, $\tau$ a valuation of
  $\ox$ with $\models \langle \tau \rangle \implies \Phi$, and
  $\langle \sigma \rangle = \mathsf{GeneralizeSat} (\Phi, \langle \tau
  \rangle)$. Then for every cube $\langle \kappa \rangle \supseteq
  \langle \sigma \rangle$, $\models \langle \kappa \rangle \implies
  \Phi$.
  \label{proposition:generalizesat}
\end{proposition}

Let $\tau \models F_k \wedge \neg P$. 
Algorithm~\ref{algorithm:optimized-property-directed-reachability}
obtains a subcube $\langle \tau_p \rangle = \mathsf{GeneralizeSat}
(F_k \wedge \neg P, \langle \tau \rangle)$. By
Proposition~\ref{proposition:generalizesat}, $\models \kappa  \implies F_k \wedge \neg
P$ for every path $\kappa$ with $\langle \kappa \rangle \supseteq \langle \tau_p
\rangle$, which follows that $\kappa \models  F_k \wedge \neg P$.
When the optimized algorithm invokes optimized $\mathsf{BlockCube}
(k, \langle \tau_p \rangle)$ to block the subcube $\langle \tau_p \rangle$, it effectively tries to remove every path $\kappa$ with $\langle \kappa \rangle \supseteq \langle \tau_p\rangle$. 


\begin{algorithm}
  \ForEach{$1 \le i < k$}
  {
    \ForEach{$\neg \langle \tau \rangle \in F_i$}
    {
      \uIf {$\not\models
        \neg \langle \tau \rangle \wedge F_i \wedge T_1 \implies
        \neg \langle \tau' \rangle$ or
        $\not\models
        \neg \langle \tau^0 \rangle \wedge
        \neg \langle \tau^1 \rangle \wedge
        F_i^0 \wedge F_i^1 \wedge T_2 \implies
        \neg \langle \tau' \rangle$}
      {
        \textbf{continue}\;

      }
    $F_{i+1} \leftarrow F_{i+1} \cup \{ \neg \langle \tau \rangle \}$\;
\hide{
    $C_{i+1} \leftarrow C_{i+1} \cup \{\langle \tau \rangle\}$\;
    $C_i \leftarrow C_i \setminus \{\langle \tau \rangle\}$\;
}
    }
    \lIf{$F_i = F_{i+1}$} 
    {
      \Return $\TT$\;
    }
  }
  \Return $\FF$\;

  \medskip
  \caption{$\textsf{Propagate}(F_1, F_2, \ldots, F_k)$}
  \label{algorithm:propagate}
\end{algorithm}

After every path $\tau$ with $\tau \models F_k \wedge \neg P$ is
removed from $\valueof{F_k}$,
Algorithm~\ref{algorithm:optimized-property-directed-reachability}
checks if an inductive path invariant has been found. 
It propagates clauses among $F_1, F_2, \ldots, F_k$
before checking whether $F_i = F_{i+1}$ for some $i$
(Line~\ref{opdr-propagate},
Algorithm~\ref{algorithm:optimized-property-directed-reachability}). Consider 
a 
clause $\neg \langle \tau \rangle \in F_j$. If $\models \neg \langle
\tau \rangle \wedge F_j \wedge T_1 \implies \neg \langle \tau' \rangle$
and $\models \neg \langle \tau^0 \rangle \wedge \neg \langle \tau^1
\rangle \wedge F^0_j \wedge F^1_j \wedge T_2 \implies \neg \langle
\tau' \rangle$, the condition $\Pi (\PP, F_0, \ldots, F_j, F_{j+1} \cup
\{ \neg \langle \tau \rangle \}, F_{j+2}, \ldots, F_k)$ still
holds. In other words, the clause $\neg \langle \tau \rangle$ can be
added to $F_{j+1}$. The algorithm $\mathsf{Propagate} (F_1, F_2,
\ldots, F_k)$ propagates all such clauses among $F_1, F_2,
\ldots, F_k$ and checks if $F_i = F_{i+1}$ for some $i$. If so,
it returns $\TT$ to conclude the verification with
\texttt{UNREACHABLE}. Otherwise, it returns $\FF$ and the optimized
algorithm proceeds to iteration $k + 1$
(Algorithm~\ref{algorithm:propagate}). 


The optimized $\mathsf{BlockCube} (k, \langle \tau \rangle)$ is
slightly more involved (Algorithm~\ref{algorithm:optimized-blockcube}).
Its design nevertheless follows a simple principle: 
all synthesized cubes are generalized whenever possible. For
a proof 
obligation $(i, \mathit{Ob})$ with $\langle \tau \rangle \in
\mathit{Ob}$, let us revisit the scenarios when the basic algorithm
removes $\tau$ from $\valueof{F_i}$.

\begin{algorithm}[h]
  \KwIn{$k$ : $\bbfN$; $\langle \tau \rangle$ : $\tau \models F_k$
    where $\Pi (\PP, F_0, F_1, \ldots, F_k)$ holds}
  $Q \leftarrow \textsf{EmptyQueue}$\;
  add $(k, \{ \langle \tau \rangle \})$ to $Q$\;
  \While{$Q$ is not empty} {
    pop $(i, \mathit{Ob})$ with the smallest $i$ from $Q$\;
    \lIf{$i = 0$}
    {
      \Return $\FF$\;
    }
    $\mathit{Ob}', \mathit{blocked} \leftarrow \varnothing, \FF$\;
    \ForEach{$\langle \tau \rangle \in \mathit{Ob}$} {
      \lIf {$\models \langle \tau \rangle \implies I$}
      {
        \textbf{continue}\;
      }
      \uIf {$\sigma, \pi' \models
        \neg \langle \tau \rangle \wedge F_{i-1} \wedge T_1
        \wedge \langle \tau' \rangle$}
      {
        \label{blockcube-case0s}
        $\langle \sigma_p \rangle \leftarrow 
        \textsf{GeneralizeSat} (\neg \langle \tau \rangle \wedge F_{i-1} \wedge T_1 \wedge \langle
        \tau' \rangle, \langle \sigma \rangle)$\;
        $\mathit{Ob}' \leftarrow \mathit{Ob}' \cup \{ \langle \sigma_p
        \rangle \}$\;
        \label{blockcube-case0e}
      } \uElseIf {$\sigma^0, \kappa^1, \pi' \models
        \neg \langle \tau^0 \rangle \wedge
        \neg \langle \tau^1 \rangle \wedge
        F_{i-1}^0 \wedge F_{i-1}^1 \wedge T_2 \wedge
        \langle \tau' \rangle$}
      {
        \label{blockcube-case1s}
        $\langle \sigma^0_p \rangle~\leftarrow~\textsf{GeneralizeSat}(\neg \langle \tau^0 \rangle \wedge
        \neg \langle \tau^1 \rangle \wedge F^0_{i-1} \wedge F^1_{i-1}
        \wedge T_2 \wedge (\langle \kappa^1 \rangle \cup \langle \tau'
        \rangle), \langle \sigma^0 \rangle)$\;
        $\langle \kappa^1_p \rangle~\leftarrow~\textsf{GeneralizeSat}(\neg \langle \tau^0 \rangle \wedge
        \neg \langle \tau^1 \rangle \wedge F^0_{i-1} \wedge F^1_{i-1}
        \wedge T_2 \wedge (\langle \sigma^0_p \rangle \cup \langle \tau'
        \rangle), \langle \kappa^1 \rangle)$\;
        $\mathit{Ob}' \leftarrow \mathit{Ob}' \cup \{ \langle \sigma_p
        \rangle, \langle \kappa_p \rangle \}$\;
        \label{blockcube-case1e}
      } \uElse
      {
        \tcp{$\langle \tau \rangle$ is blocked }
        $\neg \langle \tau_p \rangle \leftarrow \textsf{GeneralizeClause}
        (\neg \langle \tau \rangle, F_{i-1}, T_1, T_2)$\;
        \label{blockcube-case2}
        $l \leftarrow \textsf{PushClause}
        (i, k, \neg \langle \tau_p \rangle, F_0, F_1, \ldots, F_k)$\;
        \label{blockcube-pushs}
        \lForEach{$1 \le j \le l$}
        {
          $F_j \leftarrow F_j \cup \{ \neg \langle \tau_p \rangle \}$\;
        }
        \label{blockcube-pushe}
\hide{
        $C_l \leftarrow C_l \cup \{\langle \tau_p \rangle\}$\;
}
        $\mathit{blocked} \leftarrow \TT$\;
        \textbf{break}\;
      }
    }
    \uIf{$\neg \mathit{blocked}$}
    {
      add $(i, \mathit{Ob})$ and $(i-1, \mathit{Ob}')$ to $Q$\;
    }
  }
  \Return $\TT$\;

  \medskip
  \caption{Optimized $\textsf{BlockCube}(k, \langle \tau \rangle)$}
  \label{algorithm:optimized-blockcube}
\end{algorithm}

If $\models \langle \tau \rangle \implies I$, the cube $\langle \tau
\rangle$ cannot be removed from $\valueof{F_i}$ without violating the
condition $\Pi (\PP, F_0, F_1, \ldots, F_k)$. The algorithm continues
with another cube.

When there exist paths $\sigma,\pi$ such that $\sigma, \pi' \models
\neg \langle \tau \rangle \wedge F_{i-1} \wedge T_1 \wedge \langle
\tau' \rangle$, the optimized algorithm obtains a subcube $\langle
\sigma_p \rangle$ of the cube $\langle \sigma \rangle$ by
$\mathsf{GeneralizeSat} (  \neg \langle \tau \rangle \wedge  F_{i-1} \wedge T_1 \wedge \langle \tau'
\rangle, \langle \sigma \rangle)$. The cube $\langle
\sigma_p \rangle$ has the property that $
\models \langle \sigma_p \rangle \implies \neg \langle \tau \rangle \wedge F_{i-1} \wedge T_1 \wedge
\langle \tau' \rangle$. Together with Proposition~\ref{proposition:generalizesat}, we have $
\models \langle \kappa \rangle \implies \neg \langle \tau \rangle \wedge F_{i-1} \wedge T_1 \wedge
\langle \tau' \rangle$ for every path $\kappa$ with $\langle \kappa \rangle
\supseteq \langle \sigma_p \rangle$. In order to remove $\tau$ from
$\valueof{F_i}$, every path $\kappa$ with $\langle
\kappa \rangle \supseteq \langle \sigma_p \rangle$ must be removed
from $\valueof{F_{i-1}}$. The algorithm hence puts the
cube $\langle \sigma_p \rangle$ to the set $\mathit{Ob}'$
(Line~\ref{blockcube-case0s}--\ref{blockcube-case0e},
Algorithm~\ref{algorithm:optimized-blockcube}). 

When there are paths $\sigma$, $\kappa$, and $\pi$ such that 
$\sigma^0, \kappa^1, \pi' \models \neg \langle \tau^0 \rangle \wedge
\neg \langle \tau^1 \rangle \wedge F_{i-1}^0 \wedge F_{i-1}^1 \wedge
T_2 \wedge \langle \tau' \rangle$, the optimized algorithm similarly
obtains the subcubes $\langle \sigma_p \rangle$ and $\langle \kappa_p
\rangle$ of $\langle \sigma \rangle$ and $\langle \kappa
\rangle$. 
\hide{
Observe that $\eta^0, \lambda^1, \tau' \models \neg \langle
\tau^0 \rangle \wedge \neg \langle \tau^1 \rangle \wedge F_{i-1}^0
\wedge F_{i-1}^1 \wedge T_2 \wedge \langle \tau' \rangle$ for every
cubes $\langle \eta \rangle \supseteq \langle \sigma_p \rangle$ and
$\langle \lambda \rangle \supseteq \langle \kappa_p \rangle$. In orer to
remove $\tau$ from $\valueof{F_i}$, every cubes $\langle \eta \rangle
\supseteq \langle \sigma_p \rangle$ and $\langle \lambda \rangle
\supseteq \langle \kappa_p \rangle$ must be removed from
$\valueof{F_{i-1}}$.}
The optimized algorithm then adds the subcubes
$\langle \sigma_p \rangle$ and $\langle \kappa_p \rangle$ to the set
$\mathit{Ob}'$ 
(Line~\ref{blockcube-case1s}--\ref{blockcube-case1e},
Algorithm~\ref{algorithm:optimized-blockcube}).

In the fourth scenario, we have $\models I \implies \neg \langle \tau \rangle$, $\models \neg \langle \tau \rangle
\wedge F_{i-1} \wedge T_1 \implies \neg \langle \tau' \rangle$, and
$\models \neg \langle \tau^0 \rangle \wedge \neg \langle \tau^1
\rangle \wedge F^0_{i-1} \wedge F^1_{i-1} \wedge T_2 \implies \neg
\langle \tau' \rangle$. Instead of adding the clause $\neg \langle
\tau \rangle$, the optimized algorithm puts a subclause $\neg \langle
\tau_p \rangle$ of $\neg \langle \tau \rangle$ to remove more paths
from $\valueof{F_i}$. Specifically, it computes a
subclause $\neg \langle \tau_p \rangle$
such that $\models I \implies \neg \langle \tau_p \rangle$, $\models \neg \langle \tau_p \rangle \wedge F_{i-1} \wedge
T_1 \implies \neg \langle \tau'_p \rangle$, and $\models \neg \langle
\tau^0_p \rangle \wedge \neg \langle \tau^1_p \rangle \wedge F^0_{i-1}
\wedge F^1_{i-1} \wedge T_2 \implies \neg \langle \tau'_p \rangle$
so as to add $\neg \langle \tau_p \rangle$ to $F_i$. The function
$\mathsf{GeneralizeClause} (\neg \langle \tau \rangle, F_{i-1}, T_1, T_2)$
computes such a subclause $\neg \langle \tau_p \rangle$
(Algorithm~\ref{algorithm:generalizeclause}).

\hide{
\begin{algorithm}

  $\langle \tau_p \rangle \leftarrow \langle \tau_r \rangle$\;
  \ForEach{$literal\ \in \langle \tau_r \rangle$}
  {
    $\langle \tau_p \rangle \leftarrow \langle \tau_p \rangle \setminus literal$\;
    \uIf {$\langle \tau_p \rangle, \langle \tau_u \rangle \models \Phi$}
    {
      \textbf{continue}\;
    }
    \uElse
    {
      $\langle \tau_p \rangle \leftarrow \langle \tau_p \rangle \cup literal$\;
    }
  }
  \textbf{return} $\langle \tau_p \rangle$\;
  \medskip
  \caption{$\textsf{TernarySim}(\Phi, \langle \tau_r \rangle, \langle \tau_u \rangle)$}
  \label{algorithm:ternarysim}
\end{algorithm}
}

\begin{algorithm}[t]

  \KwIn{$\neg \langle \tau \rangle$ : 
    $\models I \implies \neg \langle \tau \rangle$, 
    $\models \neg \langle \tau \rangle
    \wedge F \wedge T_1 \implies \neg \langle \tau' \rangle$, and 
    $\models \neg \langle \tau^0 \rangle \wedge \neg \langle \tau^1
    \rangle \wedge F^0 \wedge F^1 \wedge T_2 \implies \neg \langle
    \tau' \rangle$}
  $\neg \langle \sigma \rangle \leftarrow \neg \langle \tau \rangle$\;
  \ForEach{$\mathit{literal}\ \ell \in \neg \langle \tau \rangle$}
  {
    $\neg \langle \sigma \rangle \leftarrow 
    \neg \langle \sigma \rangle \setminus \{ \ell \}$\;
    \uIf {
      $\models I \implies \neg \langle \sigma \rangle$
      and
      $\models
      \neg \langle \sigma \rangle \wedge F \wedge T_1 \implies
      \neg \langle \sigma' \rangle$ and
      $\models
      \neg \langle \sigma^0 \rangle \wedge
      \neg \langle \sigma^1 \rangle \wedge
      F^0 \wedge F^1 \wedge T_2 \implies
      \neg \langle \sigma' \rangle$}
    {
      \textbf{continue}\;
    }
    \uElse
    {
      $\neg \langle \sigma \rangle \leftarrow \neg \langle \sigma
      \rangle \cup \{ \ell \}$\; 
    }
  }
  \textbf{return} $\neg \langle \sigma \rangle$\;
  \medskip
  \caption{$\textsf{GeneralizeClause}(\neg \langle \tau \rangle, F, T_1, T_2)$}
  \label{algorithm:generalizeclause}
\end{algorithm}

The algorithm $\mathsf{GeneralizeClause} (\neg \langle \tau \rangle, F,
T_1, T_2)$ proceeds as follows. 
In the algorithm, we maintain a clause $\neg \langle \sigma \rangle \subseteq \neg \langle \tau \rangle$ with the properties $\models
  I \implies \neg \langle \sigma \rangle$, $\models \neg \langle
\sigma \rangle \wedge F \wedge T_1 \implies \neg \langle \sigma'
\rangle$, and $\models \neg \langle \sigma^0 \rangle \wedge \neg
\langle \sigma^1 \rangle \wedge F^0 \wedge F^1 \wedge T_2 \implies
\neg \langle \sigma' \rangle$. 
The clause $\neg \langle \sigma
\rangle$ is first initialized to $\neg \langle \tau \rangle$. The
algorithm removes a literal from $\neg \langle \sigma \rangle$ and
verifies if the three implications still hold. If so, the algorithm
iterates with another literal. Otherwise, it reinstates the removed
literal and moves on to the next literal.
\hide{
Recall that the condition $\Pi (\PP, F_0, F_1, \ldots, F_k)$ must be
maintained. We need to find a subclause of $\neg \langle \tau \rangle$
so that the condition still holds after the path $\tau$ is removed by
adding the subclause. Any clause $\neg \langle \sigma \rangle$
fulfilling the three implications will ensure the condition.}
When
Algorithm~\ref{algorithm:generalizeclause} returns, we obtain a
subclause $\neg \langle \tau_p \rangle$ of $\neg \langle \tau \rangle$
such that $\models
  I \implies \neg \langle \tau_p \rangle$, $\models \neg \langle
\tau_p \rangle \wedge F \wedge T_1 \implies \neg \langle \tau'_p
\rangle$, and $\models \neg \langle \tau^0_p \rangle \wedge \neg
\langle \tau^1_p \rangle \wedge F^0 \wedge F^1 \wedge T_2 \implies
\neg \langle \tau'_p \rangle$. Note that the algorithm does not
compute a \emph{minimal} subclause. The size of the returned subclause
depends, for instance, on the order of literal removal. In order to
obtain a smaller subclause, our implementation invokes
Algorithm~\ref{algorithm:generalizeclause} twice. Precisely, we first
obtain a subclause $\neg \langle \tau_q \rangle$ of $\neg \langle \tau
\rangle$ by invoking $\mathsf{GeneralizeClause} (\neg \langle \tau
\rangle, F, T_1, T_2)$. Our implementation then computes a subclause
$\neg \langle \tau_p \rangle$ of $\neg \langle \tau_q \rangle$ by
invoking $\mathsf{GeneralizeClause} (\neg \langle \tau_q
\rangle, F, T_1, T_2)$, and returns $\neg \langle \tau_p \rangle$ as
a generalization of the clause $\neg \langle \tau \rangle$.

After a generalized clause $\neg \langle \tau_p \rangle$ for a blocked
cube $\langle \tau \rangle \in \mathit{Ob}$ is obtained,
$\mathsf{BlockCube} (k, \langle \tau \rangle)$
(Algorithm~\ref{algorithm:optimized-blockcube}) could remove the path
$\tau$ from $\valueof{F_i}$ by adding the clause $\neg \langle \tau_p
\rangle$ to $F_0, F_1, \ldots, F_i$. It performs yet another
optimization. Recall that $\tau \models F_{i+1}$ by the condition
$\Pi (\PP, F_0, F_1, \ldots, F_k)$. If $\tau$ appears again in another
proof obligation at $F_{i+1}$,
Algorithm~\ref{algorithm:optimized-blockcube} will have to block the
path at $F_{i+1}$. We hence would like to add the clause $\neg
\langle \tau_p \rangle$ to as many of $F_0, F_1, \ldots, F_k$ as
possible. This is achieved by
Line~\ref{blockcube-pushs}--\ref{blockcube-pushe} in
Algorithm~\ref{algorithm:optimized-blockcube}. 

\begin{algorithm}[t]
  \KwIn{$\neg \langle \tau \rangle$ : 
    $\models I \implies \neg \langle \tau \rangle$, 
    $\models \neg \langle \tau \rangle
    \wedge F_{i-1} 
    \wedge T_1 \implies \neg \langle \tau' \rangle$ and
    $\models \neg \langle \tau^0 \rangle \wedge \neg \langle \tau^1
    \rangle \wedge F^0_{i-1} \wedge F^1_{i-1} \wedge T_2 \implies \neg
    \langle \tau' \rangle$}
        $l \leftarrow i$\;
        \While{$l < k$}
        {
          \uIf {$\not\models
            \neg \langle \tau \rangle \wedge F_l \wedge T_1
            \implies \neg \langle \tau' \rangle$ or
            $\not\models
            \neg \langle \tau^0 \rangle \wedge
            \neg \langle \tau^1 \rangle \wedge
            F_l^0 \wedge F_l^1 \wedge T_2 \implies
            \neg \langle \tau' \rangle$}
          {
            \textbf{break}\;
          }
          $l\leftarrow l + 1$\;
        }
  \textbf{return} $l$\;

  \medskip
  \caption{$\textsf{PushClause}(i, k, \neg \langle \tau \rangle, F_0, F_1,
    \ldots, F_k)$}
  \label{algorithm:pushclause}
\end{algorithm}

Let $\neg \langle \tau \rangle$ be a clause. The algorithm
$\mathsf{PushClause} (i, k, \neg 
\langle \tau \rangle, F_0, F_1, \ldots, F_k)$ returns an integer $i
\leq l \leq k$ such that $\models \neg \langle \tau \rangle
\wedge F_{j-1} 
\wedge T_1 \implies \neg \langle \tau' \rangle$ and
$\models \neg \langle \tau^0 \rangle \wedge \neg \langle \tau^1
\rangle \wedge F^0_{j-1} \wedge F^1_{j-1} \wedge T_2 \implies \neg
\langle \tau' \rangle$ for every $i \leq j \leq l$
(Algorithm~\ref{algorithm:pushclause}). 
\hide{
In order to keep the condition $\Pi (\PP, F_0, F_1, \ldots, F_k)$
after adding $\neg \langle \tau \rangle$ to $F_l$, we need to check
both implications for every $i \leq j < l$. 
}
The algorithm simply iterates
from $j = i$ and checks if the clause $\neg \langle \tau \rangle$ can
be added to $F_{j+1}$. Note that the condition $\Pi (\PP, F_0, F_1,
\ldots, F_k)$ holds after the clause $\neg \langle \tau \rangle$ is
added to $F_1, \ldots, F_l$.

Finally, if the proof obligation $(i, \mathit{Ob})$ cannot be discharged,
Algorithm~\ref{algorithm:optimized-blockcube} adds $(i, \mathit{Ob})$
and the induced proof obligation $(i - 1, \mathit{Ob}')$ to the
priority queue. 

\section{Experiments}
\label{exps}



To evaluate our approach, we implemented our SAT-based algorithm and compared it with the \textsc{Moped2} model checker~\cite{EsparzaS01}. In the implementation, we use the front-end of \textsc{Moped2} to translate \textsc{Remopla}
Boolean programs into pushdown systems. Further, we use \textsc{Boolector}~\cite{BrummayerB09} to convert word-level
expression to bit-level and-inverter graph (AIG) and the \textsc{ABC} framework~\cite{BraytonM10} to manipulate AIG~\cite{EenMS07}. All experiments are conducted on an Intel Xeon 2.40 Ghz CPU with 32GB memory running Linux 2.6.18.
The timeout period and memory limit for each process are set to 2000 seconds and 1GB, respectively.
We use Boolean program benchmarks from the \textsc{Moped2} package. We consider more interesting Boolean programs by skipping those without procedure calls in the benchmarks (12 out of 35). In the benchmarks, each program has one statement labeled with ``Ok'' and another labeled with ``Error.'' The former is reachable while the latter is unreachable. For each program, we check reachability against the two labels ``Ok'' and ``Error.'' We also enlarge the
default variable size in the benchmarks to 8, 16, 32, and 64 bits to evaluate the scalability of our algorithm.


Figure~\ref{PDRExp} shows the experimental results of our implementation and the BDD-based tool \textsc{Moped2}. We ignore the cases where both tools cannot handle. In the figures, we use the symbol ``$\times$'' to denote the results for the reachable label ``Ok'' and the symbol ``$\circ$'' to denote the results for the unreachable label ``Error.'' The figures use logarithmic scale. If a case cannot be finished within the timeout period, we set its execution time to 2000 seconds in the figures. For cases that take less than 1 second, we set their execution time to 1 second. For cases running out of memory, we set their execution time to 2000 seconds and denote them by different symbols (``$\ast$'' for ``Ok'' and ``$\diamond$'' for ``Error'').

\begin{figure}[h!]
\begin{center}
\begin{minipage}[b]{0.495\linewidth}
  \includegraphics[width=1\linewidth]{figures/default.pdf}
(a) default
\end{minipage} 
\begin{minipage}[b]{0.495\linewidth}
  \includegraphics[width=1\linewidth]{figures/8bit.pdf}
    (b) 8-bits
\end{minipage}
\begin{minipage}[b]{0.495\linewidth}
  \includegraphics[width=1\linewidth]{figures/16bit.pdf}
(c) 16-bits
\end{minipage}
\begin{minipage}[b]{0.495\linewidth}
  \includegraphics[width=1\linewidth]{figures/32bit.pdf}
    (d) 32-bits
\end{minipage}
\begin{minipage}[b]{0.495\linewidth}
  \includegraphics[width=1\linewidth]{figures/64bit.pdf}
(e) 64-bits
\end{minipage}
\begin{minipage}[b]{0.495\linewidth}
\centering
  \includegraphics[width=1\linewidth]{figures/finished.pdf}
  (f)~Number~of~finished~tasks
\end{minipage}

\caption{Comparing our tool with \textsc{Moped2} using examples of different variable sizes.}
\label{PDRExp}
\end{center}
\end{figure}

When the variable size is small (Figure~\ref{PDRExp} (a)), \textsc{Moped2} runs faster than our implementation for most of the cases. However, our implementation still finishes most of the cases in reasonable time. As variable sizes increase, verification tasks become more and more difficult for \textsc{Moped2}. When the size of each variable is 8 bits (Figure~\ref{PDRExp} (b)), the result is a tie in terms of both execution time and numbers of finished tasks for \textsc{Moped2} and our implementation. When the variable size is increased to 16-bits (Figure~\ref{PDRExp} (c)), \textsc{Moped2} cannot finish most of the cases within the timeout period. For the cases of variable size equal to 32 and 64 bits (Figure~\ref{PDRExp} (d) and (e)), \textsc{Moped2} runs out of memory in all the verification tasks. This is consistent with our expectation. Normally BDD-based approaches can handle problems with only a few hundred of Boolean variables (bits). Let us consider a simple example that contains only 5 global variables and no local variables. If each variable has 32 bits, then it requires at least 320 Boolean variables to encode a PDS transition (for each variable, we need both the primed and unprimed versions in the transition formula). This is already quite difficult for BDDs. We compare the number of finished verification tasks in Figure~\ref{PDRExp} (f). From the figures, we observe that our SAT-based algorithm performs equally well on both reachable and unreachable properties. We thus do not distinguish reachable and unreachable verification tasks. For each size of variable, the total number of tested verification tasks is 46. Our implementation has a much better scalability than \textsc{Moped2} in the figure. Detailed number of experiments in Table~\ref{ExpTab} are listed in the Appendix.

At the first glance, one might have doubt that most of the dots in the figures are at the border of the figure, that is, most of the verification tasks are either finished in no time or cannot be finished. 
In our experience, the most difficult step for BDD-based approaches is to encode transitions as BDDs and compute the first forward image. If BDD-based approach  successfully finishes the step, the verification normally can be concluded in seconds. In contrast, SAT-based approaches normally require more time to verify simple tasks. This is the case in Figure~\ref{PDRExp} (a).  The verification tasks  in Figure~\ref{PDRExp} (c), (d), (f) are already too difficult for BDD-based approaches. All the dots hence appear at the top border of the figures since the BDD-based approach cannot finish the tasks in time.

In Figure~\ref{PDRExecution}, we compare the execution time of our implementation with the \textsc{Moped2}. We merge the result of both the reachable and unreachable properties because there is almost no difference in both cases should we separate them. In Figure~\ref{PDRExecution} (a), we compare their median execution time. However, when the size of variables goes to 64 bits, both tool cannot finish more than a half of the verification tasks and thus the median execution time of both becomes the maximum value. In Figure~\ref{PDRExecution} (b), we use the first quartile (the one ranked at the 12th place in our case) execution time instead. Both figures show that our implementation is also better in terms of execution time comparing to \textsc{Moped2}.

\begin{figure}[htb]
\begin{center}
\begin{minipage}[b]{0.45\linewidth}
  \includegraphics[width=1\linewidth]{figures/med.pdf}
(a) Median
\end{minipage} 
\begin{minipage}[b]{0.45\linewidth}
  \includegraphics[width=1\linewidth]{figures/firstQ.pdf}
    (b) First quartile
\end{minipage}
\caption{The median and first quartile execution time for \textsc{Moped2} and our implementation. 
The figures use logarithmic scale. If a case cannot be finished with in the timeout period or runs out of memory, we set its execution time to 2000 seconds. For cases that \textsc{Moped2} runs in 0 second, we set its execution time to 0.0001 second.}
\label{PDRExecution}
\end{center}
\end{figure}

\section{Conclusions}
\label{conclusions}

We present the first complete SAT-based algorithm for the signature reachability problem on pushdown systems. We introduce inductive path invariants and generalize proof obligations in the property directed reachability algorithm. Our algorithm solves the problem by computing over-approximations to bounded reachable paths. The experimental results suggest that our SAT-based algorithm is more scalable than the BDD-based algorithm in \textsc{Moped2}. The BDD-based fails to verify any of the verification tasks with 32- and 64-bit variables. Our algorithm finishes 45 (= 24 + 21) tasks in the categories.

It is unclear whether the property directed reachability algorithm can be extended for configuration-based reachability algorithms in~\cite{rhs:popl:1995}. Such a SAT-based algorithm may be more efficient than our symbolic path-based algorithm. We also plan to extend our SAT-based signature reachability algorithm to verify temporal logic properties on pushdown systems.

%\newpage
\bibliographystyle{abbrv}%(0.5page)
\bibliography{refs}

\newpage
\appendix
\section{Details of the Encoding}
\label{encoding}


We fix $\os$ and $\ot$ to be finite sets of Boolean \emph{state} and
\emph{stack} variables respectively. A \emph{state} in $Q$ is a valuation of
$\os$; a \emph{stack symbol} in $\Gamma$ is a valuation of $\ot$.
Define three PDS transition formulae $\chi_{\Delta_0}$ over $\os^1,\ot^1,\os^2$ (pop operation), $\chi_{\Delta_1}$  over $\os^1,\ot^1,\os^2,\ot^2$ (intra-procedure operation), $\chi_{\Delta_2}$ over $\os^1,\ot^1,\os^2,\ot^2,\ot^3$ (push operation) as follows. We use $p^1, a^1, q^2, a^2, b^3$ to denote valuations of variables in $\os^1,\ot^1,\os^2,\ot^2,\ot^3$, respectively.

\begin{enumerate}
\item $p^1, a^1, q^2\models \chi_{\Delta_0}$ iff $(p,a, q) \in \Delta$\\
\item $p^1, a^1, q^2, a^2\models \chi_{\Delta_1}$ iff $(p,a, q,a) \in \Delta$\\
\item $p^1, a^1, q^2, a^2, b^3\models \chi_{\Delta_2}$ iff $(p,a, q, ab) \in \Delta$\\
\end{enumerate}

Below we explain how to encode the three RHS transition rules formulae $T_1$ over $\op,\op'$ and $T_2$ over $\op^1,\op^2,\op'$. We partition path variables $\op$ into four parts, the state variables at the source signature $\pss$, the stack variables at the source signature $\pst$, the state variables at the destination signature $\pds$, and the stack variables at the destination signature $\pds$.

We define the substitution operation that will be used in the encoding.  Let $F$ be a Boolean formula. We use $F[x \mapsfrom x']$ to denote the formula obtained by substituting all free occurrences of $x$ in $F$ with $x'$ and write $F[x_1,x_2,\ldots, x_n \mapsfrom x'_1,x'_2,\ldots, x'_n]$ as a shorthand for  $F[x_1 \mapsfrom x_1'][x_2 \mapsfrom x_2']\ldots[x_n \mapsfrom x_n']$. We lift the notation of substitution to set of variables and their variants (e.g., primed, with an index) in the natural way. 

Then $T_1$ and $T_2$ can be encoded as follows.
\[
\begin{array}{cclr}
  T_1&  \triangleq &  (\chi_{\Delta_1}[ \os^1,\ot^1,\os^2,\ot^2\mapsfrom \pds,\pdt, \pds',\pdt']  &\mbox{\textbf{(Intra-procedure rule)}}\\
  &   &   \wedge \pss= \pss'\wedge \pst=\pst') \vee&\\
  &   &   (\exists \ot_3.\chi_{\Delta_2}[ \os^1,\ot^1,\os^2,\ot^2\mapsfrom \pds,\pdt, \pds',\pdt']& \mbox{\textbf{(Push rule)}}\\
  &   &\wedge \pss'= \pds'\wedge \pst'=\pdt')&
\end{array}
\]

\[
\begin{array}{cclr}
  T_2&  \triangleq &  (\chi_{\Delta_2}[ \os^1,\ot^1,\os^2,\ot^2, \ot^3 \mapsfrom \pds^1,\pdt^1,\pss^2,\pst^2, \pdt']&\\
  &   &   \wedge \chi_{\Delta_0}[ \os^1,\ot^1,\os^2 \mapsfrom \pds^2,\pdt^2, \pds'] &\\
  &   &   \wedge \pss^{1}= \pss'\wedge \pst^1=\pst'&\mbox{\textbf{(Summary rule)}}
\end{array}
\]

\section{Details Numbers of the Experimental Results}
\label{expdetail}
Table~\ref{ExpTab} shows the details results for each benchmark example. In columns 32 and 64 bits, some results are unavailable (``-'') because the \textsc{Moped2} front-end does not allow us to increase the variable size to 32 or 64 for these cases (parsing errors occur).
In the available results of 32 and 64 bits, our approach outperforms \textsc{Moped2} in 
both reachable and unreachable properties for all the examples.

\begin{table}[htbp]
  \centering

\resizebox{0.9\columnwidth}{!}{%
    \begin{tabular}{|c|c|c|c|c|c|c|c|c|c|c|c|}    
    \hline
    Remopla      &  Tool     & \multicolumn{2}{c|}{Default} & \multicolumn{2}{c|}{8 Bits} & \multicolumn{2}{c|}{16 Bits} & \multicolumn{2}{c|}{32 Bits} & \multicolumn{2}{c|}{64 Bits}  \\
    \cline{3-12}
    Programs      &       & Error & Ok    & Error & Ok    & Error & Ok    & Error & Ok    & Error & Ok \\
    \hline
    \hline

    \texttt{blast1.rem }& \textsc{Moped} & 0.09  & 0     & 27.82 & 0.62  & T/O   & T/O   & M/O   & M/O   & M/O   & M/O \\
          & \textsc{PDR}  & 0.36  & 0.77  & 0.74  & 1.44  & 2.93  & 5.33  & 7.41  & 28.87 & 67.34 & 112.74 \\
    \hline
    \texttt{callCall2.rem} & \textsc{Moped} & 0     & 0     & 0.01  & 0.03  & 186.72 & 207.34 & - & - & - & - \\
          & \textsc{PDR}  & 0.04  & 0.04  & 0.04  & 0.27  & 0.04  & M/O   & - & - & - & - \\
    \hline
    \texttt{callCall.rem} & \textsc{Moped} & 0     & 0     & 0.01  & 0.03  & 186.94 & 212.83 & - & - & - & - \\
          & \textsc{PDR}  & 0.04  & 0.05  & 0.04  & 0.29  & 0.04  & M/O   & - & - & - & - \\
    \hline
    \texttt{callP.rem} & \textsc{Moped} & 0     & 0     & 0     & 0.01  & 181.98 & 189.06 & - & - & - & - \\
          & \textsc{PDR}  & 0.04  & 0.08  & 0.04  & 1.77  & 0.05  & M/O   & - & - & - & - \\
    \hline
    \texttt{callPReturn.rem} & \textsc{Moped} & 0     & 0     & 0     & 0.01  & 186.88 & 195.34 & - & - & - & - \\
          & \textsc{PDR}  & 0.05  & 0.05  & 0.06  & 0.43  & 0.12  & 748.03 & - & - & - & - \\
    \hline
    \texttt{call.rem} & \textsc{Moped} & 0     & 0     & 0     & 0.01  & 194.05 & 183.73 & - & - & - & - \\
          & \textsc{PDR}  & 0.04  & 0.12  & 0.04  & 0.81  & 0.06  & M/O   & - & - & - & - \\
    \hline
    \texttt{callReturn.rem} & \textsc{Moped} & 0     & 0     & 0.01  & 0     & 186.67 & 180.23 & M/O   & M/O   & M/O   & M/O \\
          & \textsc{PDR}  & 0.05  & 0.04  & 0.07  & 0.04  & 0.13  & 0.06  & 0.35  & 0.13  & 1.32  & 0.67 \\
    \hline
    \texttt{chaosGlobal.rem} & \textsc{Moped} & M/O   & 0.01  & T/O   & 200.3 & T/O   & T/O   & M/O   & M/O   & M/O   & M/O \\
          & \textsc{PDR}  & 0.25  & 0.16  & 1.52  & 0.34  & 15.81 & 2.83  & 178.08 & 17.09 & 1175.94 & 38.28 \\
    \hline
    \texttt{chaos.rem} & \textsc{Moped} & M/O   & 0.01  & T/O   & 203.33 & T/O   & T/O   & M/O   & M/O   & M/O   & M/O \\
          & \textsc{PDR}  & 0.05  & 0.08  & 0.06  & 0.33  & 0.17  & 1.57  & 0.5   & 7.95  & 2.89  & 36.42 \\
    \hline
    \texttt{critAlloc.rem2} & \textsc{Moped} & 0.79  & 0.8   & 5.32  & 5.09  & T/O   & T/O   & M/O   & M/O   & M/O   & M/O \\
          & \textsc{PDR}  & 60.82 & 0.04  & T/O   & 0.05  & 515.37 & 0.06  & T/O   & 0.08  & T/O   & 0.09 \\
    \hline
    \texttt{fac.rem} & \textsc{Moped} & 0     & 0     & 0.79  & 0.76  & T/O   & T/O   & M/O   & M/O   & M/O   & M/O \\
          & \textsc{PDR}  & 0.45  & 0.08  & 0.89  & 0.13  & 7.15  & 0.46  & 91.78 & 16.67 & T/O   & T/O \\
    \hline
    \texttt{fib.rem} & \textsc{Moped} & 0     & 0.02  & 1.01  & 1.07  & T/O   & T/O   & M/O   & M/O   & M/O   & M/O \\
          & \textsc{PDR}  & 8.19  & 3.92  & 18.72 & 7.6   & 36.4  & 35.09 & 167.52 & 64.93 & 1380.04 & 419.25 \\
    \hline
    \texttt{filesEOF.rem} & \textsc{Moped} & 0.11  & 0.14  & 0.56  & 0.67  & T/O   & T/O   & M/O   & M/O   & M/O   & M/O \\
          & \textsc{PDR}  & 1.09  & 0.89  & 0.67  & 1.2   & 1.79  & 2.64  & 1.97  & 17.82 & 3.47  & 31.73 \\
    \hline
    \texttt{files.rem} & \textsc{Moped} & 69.12 & 72.51 & 66.29 & 73.61 & T/O   & T/O   & M/O   & M/O   & M/O   & M/O \\
          & \textsc{PDR}  & 1.01  & 1.53  & 1.06  & 1.57  & 1.16  & 3.41  & 1.67  & 8.97  & 30.83 & 38.63 \\
    \hline
    \texttt{inc.rem} & \textsc{Moped} & 0     & 0     & 0.03  & 0.04  & T/O   & T/O   & M/O   & M/O   & M/O   & M/O \\
          & \textsc{PDR}  & 0.12  & 0.05  & 0.29  & 0.07  & 1.12  & 0.17  & 6.31  & 0.39  & 44.77 & 3.29 \\
    \hline
    \texttt{intInt.rem} & \textsc{Moped} & 2.65  & 0     & T/O   & 3.83  & T/O   & T/O   & M/O   & M/O   & M/O   & M/O \\
          & \textsc{PDR}  & 1.73  & 0.12  & 1119.76 & 0.6   & T/O   & 2.04  & T/O   & 10.49 & T/O   & 54.41 \\
    \hline
    \texttt{parity.rem} & \textsc{Moped} & 0.01  & 0.03  & 1.8   & 1.97  & T/O   & T/O   & - & - & - & - \\
          & \textsc{PDR}  & 2.41  & 9.92  & T/O   & T/O   & T/O   & T/O   & - & - & - & - \\
    \hline
    \texttt{qsort3Mini.rem} & \textsc{Moped} & 0     & 0     & 1.96  & 2.01  & T/O   & T/O   & M/O   & M/O   & M/O   & M/O \\
          & \textsc{PDR}  & 62.5  & 8.81  & T/O   & 128.64 & T/O   & 444.13 & T/O   & 132.35 & T/O   & T/O \\
    \hline
    \texttt{slam1.rem} & \textsc{Moped} & 0.05  & 0     & 12.61 & 0.54  & T/O   & T/O   & M/O   & M/O   & M/O   & M/O \\
          & \textsc{PDR}  & 0.42  & 0.34  & 0.64  & 0.99  & 1.79  & 2.19  & 5.79  & 10.48 & 37.29 & 30.85 \\
    \hline
    \texttt{unsinnQsort3.rem} & \textsc{Moped} & 0.09  & 0.07  & M/O   & M/O   & T/O   & T/O   & M/O   & M/O   & M/O   & M/O \\
          & \textsc{PDR}  & 0.06  & T/O   & 0.18  & T/O   & 0.36  & T/O   & 1.89  & T/O   & 9.76  & T/O \\
    \hline
    \texttt{unsinnRelDA.rem} & \textsc{Moped} & 0.08  & 0.08  & M/O   & M/O   & T/O   & T/O   & M/O   & M/O   & M/O   & M/O \\
          & \textsc{PDR}  & 0.88  & 857.58 & 8.06  & T/O   & 21.33 & T/O   & T/O   & T/O   & T/O   & T/O \\
    \hline
    \texttt{unsinnReloaded.rem} & \textsc{Moped} & 0.45  & 0.19  & M/O   & M/O   & T/O   & T/O   & M/O   & M/O   & M/O   & M/O \\
          & \textsc{PDR}  & T/O   & T/O   & T/O   & T/O   & 500.8 & T/O   & T/O   & T/O   & T/O   & T/O \\
    \hline
    \texttt{unsinn.rem} & \textsc{Moped} & 0     & 0     & 0     & 0     & 189.97 & 189.03 & - & - & - & - \\
          & \textsc{PDR}  & 0.04  & 0.05  & 0.07  & 0.05  & 0.06  & 0.04  & - & - & - & - \\
    \hline
    \end{tabular}%
    }
  \caption{Experimental results for Boolean programs with procedures or recursive functions. T/O = ``time out''. M/O = ``out of memory''. - = ``not supported by the Moped front-end'.}
  \label{ExpTab}%
\end{table}%


\end{document}

